#!/bin/tcsh
echo -n "% Problem    : " ; head -2 $1 | tail -1 | sed -e "s/.*  : //"
set ProblemSPC=`grep " SPC " $1 | sed -e "s/.* : //"`
set defaultargs="--delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --free-numbers"
set flags=" --simul-paramod --presat-simplify --forward-context-sr --strong-destructive-er --destructive-er-aggressive --destructive-er -tLPO4 -Ginvfreq -F1 -WSelectMaxLComplexAvoidPosPred -WSelectMaxLComplexAvoidPosPred "
set satflags=" --satcheck-proc-interval=5000 --satcheck=ConjMinMinFreq "
set heuristic=" -H(1.ConjectureRelativeSymbolWeight(SimulateSOS,0.5,100,100,100,100,1.5,1.5,1),4.ConjectureRelativeSymbolWeight(ConstPrio,0.1,100,100,100,100,1.5,1.5,1.5),1.FIFOWeight(PreferProcessed),1.ConjectureRelativeSymbolWeight(PreferNonGoals,0.5,100,100,100,100,1.5,1.5,1),4.Refinedweight(SimulateSOS,3,2,2,1.5,2)) "
set final="--cpu-limit="$STAREXEC_CPU_LIMIT" "$1
set ecmd="./eprover ""$defaultargs $flags $satflags $heuristic $final"

if ( "$2" == "json" ) then
    $ecmd --print-strategy > confs/$0
else
    if ( `expr "$ProblemSPC" : "TH0.*"` ) then
        echo "% Command    : " $ecmd
        /home/starexec/bin/GetComputerInfo -p THIS Model CPUModel RAMPerCPU OS | \
            sed -e "s/Computer     /% Computer   /" \
                -e "s/Model        /% Model      /" \
                -e "s/CPUModel     /% CPU        /" \
                -e "s/RAMPerCPU    /% Memory     /" \
                -e "s/OS           /% OS         /"
        echo -n "% CPULimit   : " ; echo "$STAREXEC_CPU_LIMIT"
        echo -n "% DateTime   : " ; date
        echo "% CPUTime    : "
        $ecmd
    else
        echo "% SZS status Inappropriate"
    endif
endif
